Storm 1.5.1
Date: Tue Mar 17 12:27:53 2020
Command line arguments: --prism nand.prism --prop nand.props reliable --constants 'N=60,K=4' --exact --engine portfolio --ddlib sylvan '--sylvan:maxmem' 6114 '--sylvan:threads' 4
Current working directory: /
Time for model input parsing: 0.003s.
Portfolio engine picked the following settings:
engine=hybrid bisimulation=false exact=true
Time for model construction: 1.524s.
--------------------------------------------------------------
Model type: DTMC (symbolic)
States: 18826082 (14593 nodes)
Transitions: 29772212 (97452 nodes)
Reward Models: none
Variables: rows: 8 meta variables (33 DD variables), columns: 8 meta variables (33 DD variables)
Labels: 2
* deadlock -> 0 state(s) (1 nodes)
* init -> 1 state(s) (34 nodes)
--------------------------------------------------------------
Model checking property "reliable": P=? [F ((s = 4) & ((z / 60) < 1/10))] ...
Result (for initial states): 674375412048286579998391053568044024839796891188436079164933195932504006859863176668618453626567200815744325954013096026732016576292941767289283443813273798927471369808814227780678597502526283170376011143732046040738638479975488052191318262796730887423499092060055764460808570555973414684635167757065338750791739331293858988603042989487945582955712491974590260039905065741873854885714298872588020623965467400282885463166739143535812717697199273310102277971278786945528949661789220074183715013841242260836804042248270660085557976363578175644872898551287821380993759020250450057165990145439180550980345336796910958837967490732422873158833390335926967641639016077401593504779192627736207826140866888177394711176343476439862638983111578860864406915339169201668448685867985486117826497430887145901618112836384648567977530826248389205029495657410593836586948449805252838334427173444580925770987996143922689432502457408017259242081442839253964797127083172809304607437564123586401108004199299044292446541/982021754656721722716655706411222385507669639910781715967345406263201783692889897878427213212990938612763788231403389744767067663614743521859183275654310118412922964549494284527781431535499684177432434122301448144083942764451247133599577036672904647064298810598161393171352158933989819282448394583468262131119361851408297476380158691952302398288740119725979550137284712658047394731931729250052156222114008241553695693345821266964444821100463081039235040824849892155915658833109729829406529861748248993399079598686019016345103724868380607355278949134904844556514833763239300674164534870820578969104145515316399053092033353590698921512459580587666964268557149107720604442375672662685956383159528500472087293439870951895677831469622118461029958936824764580705546202761417280408696752629675501504845173358369477857440457221826064912064573000278911442195364772677516118775811496516055643960074429058958872529316863619897048920392990112304687500000000000000000000000000000000000000000000000000000000000 (approx. 0.6867214589)
Time for model checking: 1082.562s.